| Ident. | Authors (with country if any) | Title |
|---|
| 001450 |
Clara Bertolissi [France, Italie] ; Silvio Ranise [Italie] | Verification of Composed Array-Based Systems with Applications to Security-Aware Workflows |
| 002815 |
Christopher Lynch [États-Unis] ; Silvio Ranise [Italie] ; Christophe Ringeissen [France] ; Duc-Khanh Tran [Namibie] | Automatic decidability and combinability |
| 003899 |
David Déharbe [Brésil] ; Silvio Ranise [Italie, France] | Satisfiability solving for software verification |
| 004290 |
Silvio Ghilardi [Italie] ; Enrica Nicolini [France] ; Silvio Ranise [Italie, France] ; Daniele Zucchelli [Italie] | Towards SMT Model Checking of Array-Based Systems |
| 004C19 |
Silvio Ghilardi [Italie] ; Enrica Nicolini [France] ; Silvio Ranise [France] ; Daniele Zucchelli [Italie, France] | Noetherianity and Combination Problems |
| 004C79 |
Silvio Ghilardi [Italie] ; Enrica Nicolini [France] ; Silvio Ranise [France] ; Daniele Zucchelli [Italie, France] | Decision procedures for extensions of the theory of arrays |
| 004C89 |
Silvio Ranise ; Christophe Ringeissen ; Duc-Khanh Tran | Combining Proof-Producing Decision Procedures |
| 004C91 |
Silvio Ghilardi [Italie] ; Enrica Nicolini [France] ; Silvio Ranise [France] ; Daniele Zucchelli [Italie, France] | Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems |
| 004C95 |
Silvio Ranise [France] ; Christelle Scharff [États-Unis] | Building Extended Canonizers by Graph-Based Deduction |
| 005507 |
David Déharbe [Brésil] ; Pascal Fontaine [France] ; Silvio Ranise [France, Italie] ; Christophe Ringeissen [France] | Decision Procedures for the Formal Analysis of Software |
| 005509 |
Silvio Ghilardi [Italie] ; Enrica Nicolini [Italie] ; Silvio Ranise [Italie, France] ; Daniele Zucchelli [Italie, France] | Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies |
| 005510 |
Maria Paola Bonacina [Italie] ; Silvio Ghilardi [Italie] ; Enrica Nicolini [Italie] ; Silvio Ranise [Italie, France] ; Daniele Zucchelli [Italie, France] | Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures |
| 005528 |
Hélène Kirchner ; Silvio Ranise ; Christophe Ringeissen ; Duc-Khanh Tran | Automatic Combinability of Rewriting-Based Satisfiability Procedures |
| 005607 |
Marco Bozzano [Italie] ; Roberto Bruttomesso [Italie] ; Alessandro Cimatti [Italie] ; Tommi Junttila [Finlande] ; Silvio Ranise [France] ; Peter Van Rossum [Pays-Bas] ; Roberto Sebastiani [Italie] | Efficient theory combination via boolean search |
| 005613 |
Silvio Ghilardi [Italie] ; Enrica Nicolini [Italie] ; Silvio Ranise [Italie, France] ; Daniele Zucchelli [Italie, France] | Deciding extensions of the theory of arrays by integrating decision procedures and instantiation strategies |
| 005614 |
Maria Paola Bonacina [Italie] ; Silvio Ghilardi [Italie] ; Enrica Nicolini [Italie] ; Silvio Ranise [Italie, France] ; Daniele Zucchelli [Italie, France] | Decidability and undecidability results for nelson-oppen and rewrite-based decision procedures |
| 005D31 |
Silvio Ranise ; Christophe Ringeissen ; Calogero Zarba | Combining data structures with nonstably infinite theories using many-sorted logic |
| 005E00 |
Pascal Fontaine ; Silvio Ranise ; Calogero Zarba | Combining Lists with Non-Stably Infinite Theories |
| 005E25 |
Hélène Kirchner ; Silvio Ranise ; Christophe Ringeissen ; Duc-Khanh Tran | On Superposition-Based Satisfiability Procedures and their Combination |
| 006203 |
Alessandro Armando [Italie] ; Luca Compagna [Italie] ; Silvio Ranise [France] | R ewrite and D ecision Procedure L aboratory: Combining Rewriting, Satisfiability Checking, and Lemma Speculation |
| 006222 |
Alessandro Armando [Italie] ; Maria Paola Bonacina [Italie] ; Silvio Ranise [France] ; Stephan Schulz [Italie] | On a Rewriting Approach to Satisfiability Procedures: Extension, Combination of Theories and an Experimental Appraisal |
| 006223 |
Hélène Kirchner ; Silvio Ranise ; Christophe Ringeissen ; Duc Khanh Tran | On Superposition-Based Satisfiability Procedures and Their Combination |
| 006225 |
Silvio Ranise [France] ; Christophe Ringeissen [France] ; Duc-Khanh Tran [France] | Nelson-Oppen, Shostak and the Extended Canonizer: A Family Picture with a Newborn |
| 006263 |
Marco Bozzano [Italie] ; Roberto Bruttomesso [Italie] ; Alessandro Cimatti [Italie] ; Tommi Junttila [Finlande] ; Silvio Ranise [France] ; Peter Van Rossum [Pays-Bas] ; Roberto Sebastiani [Italie] | Efficient Satisfiability Modulo Theories via Delayed Theory Combination |
| 006288 |
Silvio Ranise ; Christophe Ringeissen ; Calogero G. Zarba | Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic |
| 006375 |
Pascal Fontaine [France] ; Silvio Ranise [France] ; Calogero G. Zarba [France] | Combining lists with non-stably infinite theories |
| 006912 |
Silvio Ranise ; Christophe Ringeissen ; Duc-Khanh Tran | Nelson-Oppen, Shostak and the Extended Canonizer : A Family Picture with a Newborn |
| 006C48 |
David Déharbe [Brésil] ; Abdessamad Imine [France] ; Silvio Ranise [France] | Abstraction-Driven Verification of Array Programs |
| 007B76 |
Alessandro Armando [Italie] ; Silvio Ranise [Italie, France] ; Michaël Rusinowitch [France] | A rewriting approach to satisfiability procedures |
| 008145 |
Silvio Ranise | Etudes des principes fondamentaux de l'intégration des procédures de décisions en déduction automatique |
| 008825 |
Silvio Ranise [France] | Combining Generic and Domain Specific Reasoning by Using Contexts |
| 008C62 |
Alessandro Armando ; Silvio Ranise [France] ; Michaël Rusinowitch [France] | Uniform Derivation of Decision Procedures by Superposition |
| 009040 |
Alessandro Armando ; Silvio Ranise ; Michael Rusinowitch | Uniform Derivation of Decision Procedures by Superposition |
| 009256 |
Alessandro Armando [Italie] ; Silvio Ranise [Italie, France] ; Michaël Rusinowitch [France] | Uniform Derivation of Decision Procedures by Superposition |
| 009266 |
Alessandro Armando [Italie] ; Felice Peccia [Italie] ; Silvio Ranise [Italie, France] | The Phase Transition of the Linear Inequalities Problem |
| 009268 |
Alessandro Armando [Italie] ; Alessandro Coglio [États-Unis] ; Fausto Giunchiglia [Italie] ; Silvio Ranise [Italie] | The Control Layer in Open Mechanized Reasoning Systems: Annotations and Tactics |
| 009273 |
Alessandro Armando [Italie] ; Luca Compagna [Italie] ; Silvio Ranise [Italie, France] | System Description: RDL Rewrite and Decision Procedure Laboratory |
| 009541 |
Alessandro Armando ; Silvio Ranise [France] ; Michaël Rusinowitch [France] | Uniform Derivation of Decision Procedures by Superposition |
| 009E19 |
Alessandro Armando [Italie] ; Silvio Ranise [Italie] | Termination of Constraint Contextual Rewriting |
